T:Type, L1, L2:(T List). L1  L2  {x:T. (x  L1)  (x  L2)} 

latex

Definitions	False, A, , i  j < k, A  B, t  T, A c B, , P & Q, {i..j}, x:A. B(x), (x  l), {T}, P  Q, x:A. B(x), L1  L2
Lemmas	sublist wf, nat wf, select wf, non neg length, int seg wf, length wf1, le wf